Trait isotope::term::Value[][src]

pub trait Value: Debug + Cons + Substitute + Typecheck + HasDependencies + TermEq + Clone {
    type ValueConsed: From<Self::Consed> + Value;
    type ValueSubstituted: From<Self::Substituted> + Value;
Show methods fn into_term_direct(self) -> Term;
fn annot(&self) -> Option<AnnotationRef<'_>>;
fn is_local_ty(&self) -> Option<bool>;
fn is_local_universe(&self) -> Option<bool>;
fn is_local_function(&self) -> Option<bool>;
fn is_local_pi(&self) -> Option<bool>;
fn is_root(&self) -> bool;
fn annotate_unchecked(
        &self,
        annot: Annotation,
        ctx: &mut impl ConsCtx + ?Sized
    ) -> Result<Option<Self::ValueConsed>, Error>;
fn is_subtype_in(
        &self,
        other: &Term,
        ctx: &mut impl TermEqCtxMut + ?Sized
    ) -> Option<bool>;
fn code(&self) -> Code;
fn untyped_code(&self) -> Code;
fn eq_term_in(
        &self,
        other: &Term,
        ctx: &mut impl TermEqCtxMut + ?Sized
    ) -> Option<bool>;
fn form(&self) -> Form; fn id(&self) -> Option<NodeIx> { ... }
fn coerce(
        &self,
        ty: Option<TermId>,
        ctx: &mut impl TyCtxMut + ?Sized
    ) -> Result<Option<Self::ValueConsed>, Error> { ... }
fn coerce_id(
        &self,
        ty: Option<TermId>,
        ctx: &mut impl TyCtxMut + ?Sized
    ) -> Result<Option<TermId>, Error> { ... }
fn coerced(
        &self,
        ty: Option<TermId>,
        ctx: &mut impl TyCtxMut + ?Sized
    ) -> Result<Self::ValueConsed, Error> { ... }
fn coerced_id(
        &self,
        ty: Option<TermId>,
        ctx: &mut impl TyCtxMut + ?Sized
    ) -> Result<TermId, Error> { ... }
fn annotate_unchecked_id(
        &self,
        annot: Annotation,
        ctx: &mut impl ConsCtx + ?Sized
    ) -> Result<Option<TermId>, Error> { ... }
fn annotated_unchecked(
        &self,
        annot: Annotation,
        ctx: &mut impl ConsCtx + ?Sized
    ) -> Result<Self::ValueConsed, Error> { ... }
fn annotated_unchecked_id(
        &self,
        annot: Annotation,
        ctx: &mut impl ConsCtx + ?Sized
    ) -> Result<TermId, Error> { ... }
fn is_const(&self) -> bool { ... }
fn is_subtype(&self, other: &Term) -> Option<bool> { ... }
fn coerce_annot_ty(
        &self,
        target: &TermId,
        ctx: &mut impl TyCtxMut + ?Sized
    ) -> Result<Option<Annotation>, Error> { ... }
fn universe(&self) -> Option<Universe> { ... }
fn fn_ty(&self) -> Option<&Pi> { ... }
fn subst_rec_id(
        &self,
        ctx: &mut impl SubstCtx + ?Sized
    ) -> Result<Option<TermId>, Error> { ... }
fn subst_id(
        &self,
        ctx: &mut impl SubstCtx + ?Sized
    ) -> Result<Option<TermId>, Error> { ... }
fn shift_id(
        &self,
        n: i32,
        base: u32,
        ctx: &mut impl ConsCtx + ?Sized
    ) -> Result<Option<TermId>, Error> { ... }
fn shifted_id(
        &self,
        n: i32,
        base: u32,
        ctx: &mut impl ConsCtx + ?Sized
    ) -> Result<TermId, Error> { ... }
fn eq_id_in(
        &self,
        other: &TermId,
        ctx: &mut impl TermEqCtxMut + ?Sized
    ) -> Option<bool> { ... }
fn cons_id(&self, ctx: &mut impl ConsCtx + ?Sized) -> Option<TermId> { ... }
fn into_id_with(self, ctx: &mut impl ConsCtx + ?Sized) -> TermId { ... }
fn ty(&self) -> Option<Cow<'_, Term>> { ... }
fn ty_id(&self, ctx: &mut impl ConsCtx + ?Sized) -> Option<Cow<'_, TermId>> { ... }
fn diff_ty(&self) -> Option<&TermId> { ... }
fn base(&self) -> Option<Cow<'_, Term>> { ... }
fn base_id(
        &self,
        ctx: &mut impl ConsCtx + ?Sized
    ) -> Option<Cow<'_, TermId>> { ... }
fn apply(
        &self,
        args: &mut SmallVec<[TermId; 2]>,
        ctx: &mut impl EvalCtx + ?Sized
    ) -> Result<Option<TermId>, Error> { ... }
fn apply_ty(
        &self,
        args: &mut SmallVec<[TermId; 2]>,
        ctx: &mut impl EvalCtx + ?Sized
    ) -> Result<Option<TermId>, Error> { ... }
fn into_id_direct(self) -> TermId { ... }
fn clone_into_id_direct(&self) -> TermId { ... }
fn clone_into_id_with(&self, ctx: &mut impl ConsCtx + ?Sized) -> TermId { ... }
fn clone_into_term_direct(&self) -> Term { ... }
fn into_shallow_cons(self, ctx: &mut impl ConsCtx + ?Sized) -> TermId { ... }
fn clone_into_shallow_cons(&self, ctx: &mut impl ConsCtx + ?Sized) -> TermId { ... }
fn is_hnf(&self) -> bool { ... }
fn is_bnf(&self) -> bool { ... }
fn is_enf(&self) -> bool { ... }
fn normalize(
        &self,
        form: Form,
        max_steps: u64,
        ctx: &mut impl TyCtxMut + ?Sized
    ) -> Result<Option<TermId>, Error> { ... }
fn normalized(
        &self,
        form: Form,
        max_steps: u64,
        ctx: &mut impl TyCtxMut + ?Sized
    ) -> Result<TermId, Error> { ... }
fn reduce(
        &self,
        cfg: impl ReductionConfig,
        ctx: &mut impl TyCtxMut + ?Sized
    ) -> Result<Option<TermId>, Error> { ... }
fn reduced(
        &self,
        cfg: impl ReductionConfig,
        ctx: &mut impl TyCtxMut + ?Sized
    ) -> Result<TermId, Error> { ... }
fn reduce_until(
        &self,
        reduce: impl ReductionConfig,
        until: impl TerminationCondition,
        ctx: &mut impl TyCtxMut + ?Sized
    ) -> Result<Option<TermId>, Error> { ... }
fn reduced_until(
        &self,
        reduce: impl ReductionConfig,
        until: impl TerminationCondition,
        ctx: &mut impl TyCtxMut + ?Sized
    ) -> Result<TermId, Error> { ... }
}
Expand description

A trait implemented by values in isotope’s term language

Associated Types

The type of value this is consed to

The type of value this is substituted to

Required methods

Convert this term to a Term, without any consing

Get the type annotation of this term

Get whether this term is a type

Get whether this term is a universe

Get whether this term is a function

Get whether this term is a dependent function type

Get whether this term is in “root form”

Convert this term to an annotation, with only rudimentary type-checking

Get whether this term is a subtype of another in a given context

Get the hash-code of this term

It is an invariant that, if two terms t, u differ only due to typing annotations for any subterm, t.code().pure() == u.code.pure().

Get the hash-code of this term if it was untyped

This can be helpful in, e.g., looking up the untyped term in a hash-map when one only has the typed term. It is an invariant that, for all terms t, t.code().pure() == t.untyped_code().pure(). On the other hand, it is not necessarily the case that t.ty() == None implies that t.code() == t.untyped_code(), since while t itself is not annotated, it’s subterms may be, which would affect the upper 32 bits of t.code().

Compare this term to another within a given context

Get the form of this term

Provided methods

Get the index of this term in a program graph. Return None if this term is unindexed

Coerce this term to another type, with type-checking

Coerce this term to another type, with type-checking

Coerce this term to another type, with type-checking

Coerce this term to another type, with type-checking

Convert this term to an annotation, with only rudimentary type-checking

Convert this term to an annotation, with only rudimentary type-checking

Convert this term to an annotation, with only rudimentary type-checking

Get whether this term is a constant.

Get whether this term is a subtype of another in general

Cast this type into another in a given typing context

Get whether this term has a universe in all contexts

Get whether this term has a pi type in all contexts

Substitute this term’s variables recursively given a context

Substitute this term’s variables given a context

Shift this term’s variables with index >= base up by n in a given context

Shift this term’s variables with index >= base up by n in a given context

Compare this term to a term ID, within a given context

Cons this term within a given context. Return None if already consed.

Convert this term to a TermId within a given context

Get the type of this term, if any

Get the type of this term, if any

Get the transported type of this term, if any

Get the base type of this term, if any

Get the type of this term, if any

Apply this value, as a function, to a given vector of arguments in a given context Returns None if there is no change. Pops off consumed arguments.

Apply this value, as a dependent function type, to a given vector of arguments in a given context Returns None if there is no change. Pops off consumed arguments.

Convert this term to a TermId, without any consing

Clone this term to a TermId, without any consing

Clone this term to a TermId within a given context

Clone this term to a Term without any consing

Shallow cons a term directly into a context

Shallow cons a term directly into a context, cloning if necessary

Get whether this term is in head normal form

Get whether this term is in beta normal form

Get whether this term is in eta normal form

Convert this term to a normal form

Convert this term a normal form

Convert this term to a normal form, or reduce it up to n steps

Convert this term a normal form, or reduce it up to n steps

Convert this term to a normal form, or reduce it up to n steps

Convert this term a normal form, or reduce it up to n steps

Implementations on Foreign Types

Implementors